g:OGrp, a, b:|g|. (e  a)  (e  b)  (e  (a * b)) 

latex

Up	groups 1
Definitions of Statement	IMonoid, Mon, AbMon, OCMon, OGrp
Definitions	t  T, P  Q, x:A. B(x), IMonoid, True, T, , P  Q, P & Q, P  Q, x f y, Mon, AbMon, OCMon, OGrp
Lemmas	ocgrp wf, grp car wf, grp id wf, grp leq wf, grp op wf, monoid p wf, mon ident, grp sig wf, true wf, squash wf, grp leq op l, grp leq transitivity